$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$ List), $e$:E.
\\[0ex](0 $<$ $\parallel$es{-}interface{-}history(${\it es}$;$X$;$e$)$\parallel$)
\\[0ex]$\Leftarrow\!\Rightarrow$ ($\exists$${\it e'}$:E. (($\uparrow$(${\it e'}$ $\in_{b}$ $X$)) \& ${\it e'}$ $\leq$loc $e$  \& (0 $<$ $\parallel$$X$(${\it e'}$)$\parallel$)))